/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package chameleon.model.NuGatStructure.strategy;

import chameleon.model.NuGatStructure.fsm.GameBddFsm;
import chameleon.model.NuGatStructure.game.GamePlayer;
import chameleon.model.NuGatStructure.symbTable.SymbLayer;
import chameleon.model.NuGatStructure.prop.PropGame;
import chameleon.model.NuGatStructure.utils.Node;
import chameleon.model.NuGatStructure.bdd.Bdd;
import chameleon.model.NuGatStructure.enc.BddEnc;
import chameleon.gameSolver.NuGat.NuGatInterface;
import com.sun.jna.Pointer;

/**
 *
 * @author simon
 */
public class GenReactivityStrategy extends GenBuchiStrategy {
    
    public GenReactivityStrategy(Pointer strategy,PropGame prop,Node varList1, 
            Node varList2, SymbLayer layer, NuGatInterface nugat){
        super (strategy,prop,varList1,varList2,layer,nugat);
    }

    private GenReactivityStrategy (BddEnc bdd_enc,
                     GamePlayer player,
                     int reverseInitialQuantifiers,
                     Bdd init_goal,
                     Bdd init_opponent_deadlock,
                     Bdd init_moves,
                     Bdd goal,
                     Bdd opponent_deadlock,
                     Bdd moves,
                     PropGame prop,
                     SymbLayer layer,
                     NuGatInterface nugat){
        super(nugat.GameStrategy_create(bdd_enc.ptr(),
                player.ptr(),
                reverseInitialQuantifiers,
                init_goal.ptr(),
                init_opponent_deadlock.ptr(),
                init_moves.ptr(),
                goal.ptr(),
                opponent_deadlock.ptr(),
                moves.ptr()),prop,layer, nugat);
    }
    
    @Override
    public final GenReactivityStrategy clone(){
        GenReactivityStrategy strategy =  new GenReactivityStrategy(this.getBddEnc(),
                this.getPlayer(),
                this.getReverseInitialQuantifiers(),
                this.getInitGoal(),
                this.getInitOpponentDeadlock(),
                this.getInitMoves(),
                this.getGoal(),
                this.getOpponentDeadlock(),
                this.getMoves(),prop_,getLayer(), nugat_
                );
     strategy.setVarList1(varList1_);
     strategy.setVarList2(varList2_);
     strategy.setReverseInitialQuantifiers(reverseInitialQuantifiers_);
     return strategy;
    }

    @Override
    public Node getLtlSpec() {
        Node expr = new Node(prop_.getExprCore().ptr(), nugat_);
        Node left = expr.car();
        Node right = expr.cdr();
        
        getBuchiFormula(left);
        getBuchiFormula(right);
        
        Node ltlSpec = new Node(nugat_.IMPLIES, getBuchiFormula(left), getBuchiFormula(right),
                nugat_);
        
        return ltlSpec;
        
    }

    @Override
    public boolean getSuccess(GamePlayer player, GameBddFsm fsm) {
        Node specExp = new Node(prop_.getExprCore().ptr(),nugat_);
        return (nugat_.Chameleon_game_compute_gen_reactivity(specExp.ptr(), player.getPLayer(),fsm.ptr())==1);
    }
}
